\begin{tabbing}
$\forall$$A$, $B$:Realizer.
\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ R{-}Feasible($B$)
\\[0ex]$\Rightarrow$ ($\exists$\=$i$:Id\+
\\[0ex](($\forall$$j$:Id. R{-}has{-}loc($A$;$j$) = $i$ = $j$ $\in$ $\mathbb{B}$)
\\[0ex]\& \=$\forall$$k$$\in$dom(R{-}da($A$;$i$)). \+
\\[0ex]
\\[0ex]$T$\==R{-}da($A$;$i$)($k$) $\Rightarrow$ \+
\\[0ex]($\uparrow$isrcv($k$))
\-\\[0ex]$\Rightarrow$ \=(((source(lnk($k$)) = $i$ $\in$ Id) $\Rightarrow$ ($T$ $\subseteq$r R{-}da($B$;destination(lnk($k$)))($k$)?Top))\+
\\[0ex]\& ((destination(lnk($k$)) = $i$ $\in$ Id) $\Rightarrow$ (R{-}da($B$;source(lnk($k$)))($k$)?Void $\subseteq$r $T$)))))
\-\-\-\\[0ex]$\Rightarrow$ R{-}icompat($B$;$A$)
\end{tabbing}